Inference at * 1 
Iof proof for Lemma p-conditional-to-p-first:



1. A : Type
2. B : Type
3. f : A(B + Top)
4. g : A(B + Top)
5. x : A
  [f?g](x) = p-first([f; g])(x) 

latex

 by ((RepUR ``p-conditional p-first can-apply`` 0) 
CollapseTHEN (((((GenConclAtAddr [2;1;1]) 

CCollapseTHENA (Auto))) 
CollapseTHEN (((D (-2)) 
CollapseTHEN (((Reduce 0) 
CollapseTHEN (
CAuto)))))))) 

latex

C.

Definitions	[f?g], p-first(L), can-apply(f;x), P  Q, x:A. B(x), t  T, left + right, inr x , Top, x:AB(x), Type, s = t, f(a)
Lemmas	top wf